module Lambda 

where 

data Lam = Var Int | App Lam Lam | Abs Int Lam deriving (Eq, Show)

isfree :: Int -> Lam -> Bool
isfree x (Var y) = x == y 
isfree x (App e f) = isfree x e || isfree x f
isfree x (Abs v body) = x /= v && isfree x body

firstfreshindex :: [Int] -> Int
firstfreshindex s = find 0 s 
                    where find x s | x `elem` s = find (x+1) s
                                   | otherwise = x 

frees :: Lam -> [Int]
frees (Var v) = [v]
frees (App e f) = (frees e) ++ (frees f)
frees (Abs v body) = difference (frees body) [v]

difference [] t = []
difference (s:ss) t | elem s t = difference ss t
                    | otherwise = s:(difference ss t)

subst :: Int -> Lam -> Lam -> Lam
subst x e f@(Var v)
    | x==v = e 
    | otherwise = f 
subst x e (App f g) = App (subst x e f) (subst x e g) 
subst x e f@(Abs bndvar body)
    | not (isfree x f) = f 
    | not (isfree bndvar e) = Abs bndvar (subst x e body)
    | otherwise = Abs z (subst x e (subst bndvar (Var z) body))
      where z = firstfreshindex ((frees e) ++ (frees f))

alphaRedNotion :: Lam -> Lam -> Bool
alphaRedNotion (Abs bndvar body) (Abs bndvar' body') = 
     body' == subst bndvar (Var bndvar') body
alphaRedNotion _ _ = False

alphaVariants ::  Lam -> Lam -> Bool
alphaVariants (Var i) (Var j) = i == j 
alphaVariants (Abs bndvar body) (Abs bndvar' body') = 
   alphaVariants body (subst bndvar' (Var bndvar) body')
alphaVariants (App term1 term2) (App term3 term4) =
   alphaVariants term1 term3 && alphaVariants term2 term4
alphaVariants _ _ = False 

betaRedNotion :: Lam -> Lam -> Bool
betaRedNotion (App (Abs v m) n) f = f == subst v n m 
betaRedNotion _ _ = False

etaRedNotion :: Lam -> Lam -> Bool
etaRedNotion (Abs var (App f (Var var'))) f' = 
          var == var' && not (isfree var f) && f == f' 
etaRedNotion _ _ = False

normalform :: Lam -> Bool
normalform (Var v) = True
normalform (Abs v body@(App e (Var w))) 
  | v == w && (elem w (frees e)) = False 
  | otherwise                    = normalform body
normalform (Abs v body) = normalform body
normalform (App (Var v) e) = normalform e
normalform (App (Abs v body) e) = False
normalform (App (App e f) g) = normalform (App e f) && normalform g

startswithvar :: Lam -> Bool
startswithvar (Var v) = True 
startswithvar (Abs v body) = False
startswithvar (App e f) = startswithvar e 

hnormalform :: Lam -> Bool
hnormalform (Var v) = True
hnormalform (Abs v body) = hnormalform body 
hnormalform (App e f) = startswithvar e

whnormalform :: Lam -> Bool
whnormalform (Var v) = True
whnormalform (Abs v body) = True
whnormalform (App e f) = startswithvar e

nf :: Lam -> Lam
nf term = nf_ba term [] []

nf_ba :: Lam -> [Int] -> [Lam] -> Lam
nf_ba (Var v) vars args = compose (Var v) vars args
nf_ba (Abs v body) vars [] = nf_ba body (v:vars) [] 
nf_ba (Abs v body) vars (f:args) = nf_ba (subst v f body) vars args
nf_ba (App e f) vars args = nf_ba e vars ((nf f):args)

compose term [] [] = term 
compose term (v:vars) [] = compose (Abs v term) vars []
compose term vars (a:args) = compose (App term a) vars args

nf_lr :: Lam -> Lam
nf_lr term = nf_lr_ba term [] []

nf_lr_ba :: Lam -> [Int] -> [Lam] -> Lam
nf_lr_ba (Var v) vars args = compose_nf (Var v) vars args
    where 
    compose_nf term [] [] = term 
    compose_nf term (v:vars) [] = 
         compose_nf (Abs v term) vars []
    compose_nf term vars (a:args) = 
         compose_nf (App term (nf_lr a)) vars args
nf_lr_ba (Abs v body) vars [] = nf_lr_ba body (v:vars) [] 
nf_lr_ba (Abs v body) vars (f:args) = nf_lr_ba (subst v f body) vars args
nf_lr_ba (App e f) vars args = nf_lr_ba e vars (f:args)

hnf :: Lam -> Lam
hnf term = hnf_ba term [] []
   
hnf_ba :: Lam -> [Int] -> [Lam] -> Lam
hnf_ba (Var v) vars args = compose (Var v) vars args
hnf_ba (Abs v body) vars [] = hnf_ba body (v:vars) [] 
hnf_ba (Abs v body) vars (f:args) = hnf_ba (subst v f body) vars args
hnf_ba (App e f) vars args = hnf_ba e vars (f:args)

whnf :: Lam -> Lam
whnf term = whnf_ba term [] []
   
whnf_ba :: Lam -> [Int] -> [Lam] -> Lam
whnf_ba (Var v) vars args = compose (Var v) vars args
whnf_ba (Abs v body) vars [] = compose (Abs v body) vars [] 
whnf_ba (Abs v body) vars (f:args) = whnf_ba (subst v f body) vars args
whnf_ba (App e f) vars args = whnf_ba e vars (f:args)

k     = (Abs 1 (Abs 2 (Var 1)))
i     = (Abs 1 (Var 1))
s     = (Abs 1 (Abs 2 (Abs 3 
            (App (App (Var 1) (Var 3)) (App (Var 2) (Var 3))))))
omega = (App (Abs 1 (App (Var 1) (Var 1))) 
            (Abs 1 (App (Var 1) (Var 1))))

y     = (Abs 1 (App (Abs 2 (App (Var 1) (App (Var 2) (Var 2))))
                    (Abs 2 (App (Var 1) (App (Var 2) (Var 2))))))

skk   = (App (App s k) k)
sk    = (App s k)
b     = (App (App s (App k s)) k)
ik    = (App i k)
b'    = (App (App (App b (Var 1)) (Var 2)) (Var 3))

cn n = (Abs 1 (Abs 0 (cn_body n)))

cn_body 0 = (Var 0)
cn_body (n+1) = (App (Var 1) (cn_body n))

one = cn 1 
two = cn 2 
three = cn 3
four = cn 4

number (Abs 1 (Abs 0 (Var 0))) = 0 
number (Abs 1 (Abs 0 (App (Var 1) term)))  = 
       (number (Abs 1 (Abs 0 term))) + 1

plus = (Abs 1 (Abs 2 (Abs 3 (Abs 4 
       (App (App (Var 1) (Var 3))
            (App (App (Var 2) (Var 3)) (Var 4)))))))

expo = (Abs 1 (Abs 2 (App (Var 2) (Var 1))))

expo22 = (App (App expo two) two)

expo33 = (App (App expo three) three)

showLam :: Lam -> String
showLam term = showsLam term ""

-- showsLam : print with explicit binder, without outer parentheses

showsLam :: Lam -> String -> String 
showsLam (Abs v term) string = '^': shows v (showsLam1 term string)
showsLam (App e f) string = showsLam e (showsLam2 f string)
showsLam (Var v) string = shows v string 

-- showsLam1 : abstractions without and applications with outer parentheses

showsLam1 :: Lam -> String -> String 
showsLam1 (Abs v term) string = shows v (showsLam1 term string)
showsLam1 (App e f) string = '.' : '(' : showsLam e 
                                         (showsLam2 f  (')': string))
showsLam1 (Var v) string = '.': shows v string 

-- showsLam2 : abstractions and applications with outer parentheses

showsLam2 :: Lam -> String -> String 
showsLam2 (Abs v term) string = 
     '(' :'^': shows v (showsLam1 term (')': string))
showsLam2 (App e f) string = '(' : showsLam2 e (showsLam2 f (')':string))
showsLam2 (Var v) string = shows v string 

snf :: Lam -> String 
snf = showLam . nf 

